The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

#equal(@x, @y) → #eq(@x, @y)
#less(@x, @y) → #cklt(#compare(@x, @y))
and(@x, @y) → #and(@x, @y)
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(leq(@x, @y), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insert#2(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys))
isortlist(@l) → isortlist#1(@l)
isortlist#1(::(@x, @xs)) → insert(@x, isortlist(@xs))
isortlist#1(nil) → nil
leq(@l1, @l2) → leq#1(@l1, @l2)
leq#1(::(@x, @xs), @l2) → leq#2(@l2, @x, @xs)
leq#1(nil, @l2) → #true
leq#2(::(@y, @ys), @x, @xs) → or(#less(@x, @y), and(#equal(@x, @y), leq(@xs, @ys)))
leq#2(nil, @x, @xs) → #false
or(@x, @y) → #or(@x, @y)

The (relative) TRS S consists of the following rules:

#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)
#eq(#0, #0) → #true
#eq(#0, #neg(@y)) → #false
#eq(#0, #pos(@y)) → #false
#eq(#0, #s(@y)) → #false
#eq(#neg(@x), #0) → #false
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)
#eq(#neg(@x), #pos(@y)) → #false
#eq(#pos(@x), #0) → #false
#eq(#pos(@x), #neg(@y)) → #false
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)
#eq(#s(@x), #0) → #false
#eq(#s(@x), #s(@y)) → #eq(@x, @y)
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#eq(::(@x_1, @x_2), nil) → #false
#eq(nil, ::(@y_1, @y_2)) → #false
#eq(nil, nil) → #true
#or(#false, #false) → #false
#or(#false, #true) → #true
#or(#true, #false) → #true
#or(#true, #true) → #true

Rewrite Strategy: INNERMOST

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
insert(::(@x17874_3, @xs17875_3), ::(nil, @ys17560_3)) →⁺ ::(nil, insert(::(@x17874_3, @xs17875_3), @ys17560_3))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1].
The pumping substitution is [@ys17560_3 / ::(nil, @ys17560_3)].
The result substitution is [ ].

(2) BOUNDS(n^1, INF)

(3) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(4) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

#equal(@x, @y) → #eq(@x, @y)
#less(@x, @y) → #cklt(#compare(@x, @y))
and(@x, @y) → #and(@x, @y)
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(leq(@x, @y), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insert#2(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys))
isortlist(@l) → isortlist#1(@l)
isortlist#1(::(@x, @xs)) → insert(@x, isortlist(@xs))
isortlist#1(nil) → nil
leq(@l1, @l2) → leq#1(@l1, @l2)
leq#1(::(@x, @xs), @l2) → leq#2(@l2, @x, @xs)
leq#1(nil, @l2) → #true
leq#2(::(@y, @ys), @x, @xs) → or(#less(@x, @y), and(#equal(@x, @y), leq(@xs, @ys)))
leq#2(nil, @x, @xs) → #false
or(@x, @y) → #or(@x, @y)

The (relative) TRS S consists of the following rules:

#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)
#eq(#0, #0) → #true
#eq(#0, #neg(@y)) → #false
#eq(#0, #pos(@y)) → #false
#eq(#0, #s(@y)) → #false
#eq(#neg(@x), #0) → #false
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)
#eq(#neg(@x), #pos(@y)) → #false
#eq(#pos(@x), #0) → #false
#eq(#pos(@x), #neg(@y)) → #false
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)
#eq(#s(@x), #0) → #false
#eq(#s(@x), #s(@y)) → #eq(@x, @y)
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#eq(::(@x_1, @x_2), nil) → #false
#eq(nil, ::(@y_1, @y_2)) → #false
#eq(nil, nil) → #true
#or(#false, #false) → #false
#or(#false, #true) → #true
#or(#true, #false) → #true
#or(#true, #true) → #true

Rewrite Strategy: INNERMOST

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(6) Obligation:

Innermost TRS:
Rules:
#equal(@x, @y) → #eq(@x, @y)
#less(@x, @y) → #cklt(#compare(@x, @y))
and(@x, @y) → #and(@x, @y)
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(leq(@x, @y), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insert#2(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys))
isortlist(@l) → isortlist#1(@l)
isortlist#1(::(@x, @xs)) → insert(@x, isortlist(@xs))
isortlist#1(nil) → nil
leq(@l1, @l2) → leq#1(@l1, @l2)
leq#1(::(@x, @xs), @l2) → leq#2(@l2, @x, @xs)
leq#1(nil, @l2) → #true
leq#2(::(@y, @ys), @x, @xs) → or(#less(@x, @y), and(#equal(@x, @y), leq(@xs, @ys)))
leq#2(nil, @x, @xs) → #false
or(@x, @y) → #or(@x, @y)
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)
#eq(#0, #0) → #true
#eq(#0, #neg(@y)) → #false
#eq(#0, #pos(@y)) → #false
#eq(#0, #s(@y)) → #false
#eq(#neg(@x), #0) → #false
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)
#eq(#neg(@x), #pos(@y)) → #false
#eq(#pos(@x), #0) → #false
#eq(#pos(@x), #neg(@y)) → #false
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)
#eq(#s(@x), #0) → #false
#eq(#s(@x), #s(@y)) → #eq(@x, @y)
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#eq(::(@x_1, @x_2), nil) → #false
#eq(nil, ::(@y_1, @y_2)) → #false
#eq(nil, nil) → #true
#or(#false, #false) → #false
#or(#false, #true) → #true
#or(#true, #false) → #true
#or(#true, #true) → #true

Types:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#less :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #EQ:#GT:#LT
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
insert :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
isortlist :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
isortlist#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
leq#2 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
or :: #false:#true → #false:#true → #false:#true
#or :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_3 :: :::nil:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
gen_:::nil:#0:#neg:#pos:#s4_3 :: Nat → :::nil:#0:#neg:#pos:#s

(7) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
#eq, #compare, insert, insert#1, leq, isortlist, isortlist#1, leq#1

They will be analysed ascendingly in the following order:
insert = insert#1
insert < isortlist#1
leq < insert#1
leq = leq#1
isortlist = isortlist#1

(8) Obligation:

Innermost TRS:
Rules:
#equal(@x, @y) → #eq(@x, @y)
#less(@x, @y) → #cklt(#compare(@x, @y))
and(@x, @y) → #and(@x, @y)
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(leq(@x, @y), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insert#2(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys))
isortlist(@l) → isortlist#1(@l)
isortlist#1(::(@x, @xs)) → insert(@x, isortlist(@xs))
isortlist#1(nil) → nil
leq(@l1, @l2) → leq#1(@l1, @l2)
leq#1(::(@x, @xs), @l2) → leq#2(@l2, @x, @xs)
leq#1(nil, @l2) → #true
leq#2(::(@y, @ys), @x, @xs) → or(#less(@x, @y), and(#equal(@x, @y), leq(@xs, @ys)))
leq#2(nil, @x, @xs) → #false
or(@x, @y) → #or(@x, @y)
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)
#eq(#0, #0) → #true
#eq(#0, #neg(@y)) → #false
#eq(#0, #pos(@y)) → #false
#eq(#0, #s(@y)) → #false
#eq(#neg(@x), #0) → #false
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)
#eq(#neg(@x), #pos(@y)) → #false
#eq(#pos(@x), #0) → #false
#eq(#pos(@x), #neg(@y)) → #false
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)
#eq(#s(@x), #0) → #false
#eq(#s(@x), #s(@y)) → #eq(@x, @y)
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#eq(::(@x_1, @x_2), nil) → #false
#eq(nil, ::(@y_1, @y_2)) → #false
#eq(nil, nil) → #true
#or(#false, #false) → #false
#or(#false, #true) → #true
#or(#true, #false) → #true
#or(#true, #true) → #true

Types:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#less :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #EQ:#GT:#LT
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
insert :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
isortlist :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
isortlist#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
leq#2 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
or :: #false:#true → #false:#true → #false:#true
#or :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_3 :: :::nil:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
gen_:::nil:#0:#neg:#pos:#s4_3 :: Nat → :::nil:#0:#neg:#pos:#s

Generator Equations:
gen_:::nil:#0:#neg:#pos:#s4_3(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s4_3(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s4_3(x))

The following defined symbols remain to be analysed:
#eq, #compare, insert, insert#1, leq, isortlist, isortlist#1, leq#1

They will be analysed ascendingly in the following order:
insert = insert#1
insert < isortlist#1
leq < insert#1
leq = leq#1
isortlist = isortlist#1

(9) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3)) → #false, rt ∈ Ω(0)

Induction Base:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, 0)), gen_:::nil:#0:#neg:#pos:#s4_3(0)) →_R^Ω(0)
#false

Induction Step:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, +(n6_3, 1))), gen_:::nil:#0:#neg:#pos:#s4_3(+(n6_3, 1))) →_R^Ω(0)
#and(#eq(nil, nil), #eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3))) →_R^Ω(0)
#and(#true, #eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3))) →_IH
#and(#true, #false) →_R^Ω(0)
#false

We have rt ∈ Ω(1) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n⁰).

(10) Complex Obligation (BEST)

(11) Obligation:

Innermost TRS:
Rules:
#equal(@x, @y) → #eq(@x, @y)
#less(@x, @y) → #cklt(#compare(@x, @y))
and(@x, @y) → #and(@x, @y)
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(leq(@x, @y), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insert#2(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys))
isortlist(@l) → isortlist#1(@l)
isortlist#1(::(@x, @xs)) → insert(@x, isortlist(@xs))
isortlist#1(nil) → nil
leq(@l1, @l2) → leq#1(@l1, @l2)
leq#1(::(@x, @xs), @l2) → leq#2(@l2, @x, @xs)
leq#1(nil, @l2) → #true
leq#2(::(@y, @ys), @x, @xs) → or(#less(@x, @y), and(#equal(@x, @y), leq(@xs, @ys)))
leq#2(nil, @x, @xs) → #false
or(@x, @y) → #or(@x, @y)
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)
#eq(#0, #0) → #true
#eq(#0, #neg(@y)) → #false
#eq(#0, #pos(@y)) → #false
#eq(#0, #s(@y)) → #false
#eq(#neg(@x), #0) → #false
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)
#eq(#neg(@x), #pos(@y)) → #false
#eq(#pos(@x), #0) → #false
#eq(#pos(@x), #neg(@y)) → #false
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)
#eq(#s(@x), #0) → #false
#eq(#s(@x), #s(@y)) → #eq(@x, @y)
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#eq(::(@x_1, @x_2), nil) → #false
#eq(nil, ::(@y_1, @y_2)) → #false
#eq(nil, nil) → #true
#or(#false, #false) → #false
#or(#false, #true) → #true
#or(#true, #false) → #true
#or(#true, #true) → #true

Types:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#less :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #EQ:#GT:#LT
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
insert :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
isortlist :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
isortlist#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
leq#2 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
or :: #false:#true → #false:#true → #false:#true
#or :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_3 :: :::nil:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
gen_:::nil:#0:#neg:#pos:#s4_3 :: Nat → :::nil:#0:#neg:#pos:#s

Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3)) → #false, rt ∈ Ω(0)

Generator Equations:
gen_:::nil:#0:#neg:#pos:#s4_3(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s4_3(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s4_3(x))

The following defined symbols remain to be analysed:
#compare, insert, insert#1, leq, isortlist, isortlist#1, leq#1

They will be analysed ascendingly in the following order:
insert = insert#1
insert < isortlist#1
leq < insert#1
leq = leq#1
isortlist = isortlist#1

(12) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol #compare.

(13) Obligation:

Innermost TRS:
Rules:
#equal(@x, @y) → #eq(@x, @y)
#less(@x, @y) → #cklt(#compare(@x, @y))
and(@x, @y) → #and(@x, @y)
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(leq(@x, @y), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insert#2(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys))
isortlist(@l) → isortlist#1(@l)
isortlist#1(::(@x, @xs)) → insert(@x, isortlist(@xs))
isortlist#1(nil) → nil
leq(@l1, @l2) → leq#1(@l1, @l2)
leq#1(::(@x, @xs), @l2) → leq#2(@l2, @x, @xs)
leq#1(nil, @l2) → #true
leq#2(::(@y, @ys), @x, @xs) → or(#less(@x, @y), and(#equal(@x, @y), leq(@xs, @ys)))
leq#2(nil, @x, @xs) → #false
or(@x, @y) → #or(@x, @y)
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)
#eq(#0, #0) → #true
#eq(#0, #neg(@y)) → #false
#eq(#0, #pos(@y)) → #false
#eq(#0, #s(@y)) → #false
#eq(#neg(@x), #0) → #false
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)
#eq(#neg(@x), #pos(@y)) → #false
#eq(#pos(@x), #0) → #false
#eq(#pos(@x), #neg(@y)) → #false
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)
#eq(#s(@x), #0) → #false
#eq(#s(@x), #s(@y)) → #eq(@x, @y)
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#eq(::(@x_1, @x_2), nil) → #false
#eq(nil, ::(@y_1, @y_2)) → #false
#eq(nil, nil) → #true
#or(#false, #false) → #false
#or(#false, #true) → #true
#or(#true, #false) → #true
#or(#true, #true) → #true

Types:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#less :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #EQ:#GT:#LT
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
insert :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
isortlist :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
isortlist#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
leq#2 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
or :: #false:#true → #false:#true → #false:#true
#or :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_3 :: :::nil:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
gen_:::nil:#0:#neg:#pos:#s4_3 :: Nat → :::nil:#0:#neg:#pos:#s

Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3)) → #false, rt ∈ Ω(0)

Generator Equations:
gen_:::nil:#0:#neg:#pos:#s4_3(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s4_3(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s4_3(x))

The following defined symbols remain to be analysed:
leq#1, insert, insert#1, leq, isortlist, isortlist#1

They will be analysed ascendingly in the following order:
insert = insert#1
insert < isortlist#1
leq < insert#1
leq = leq#1
isortlist = isortlist#1

(14) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol leq#1.

(15) Obligation:

Innermost TRS:
Rules:
#equal(@x, @y) → #eq(@x, @y)
#less(@x, @y) → #cklt(#compare(@x, @y))
and(@x, @y) → #and(@x, @y)
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(leq(@x, @y), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insert#2(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys))
isortlist(@l) → isortlist#1(@l)
isortlist#1(::(@x, @xs)) → insert(@x, isortlist(@xs))
isortlist#1(nil) → nil
leq(@l1, @l2) → leq#1(@l1, @l2)
leq#1(::(@x, @xs), @l2) → leq#2(@l2, @x, @xs)
leq#1(nil, @l2) → #true
leq#2(::(@y, @ys), @x, @xs) → or(#less(@x, @y), and(#equal(@x, @y), leq(@xs, @ys)))
leq#2(nil, @x, @xs) → #false
or(@x, @y) → #or(@x, @y)
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)
#eq(#0, #0) → #true
#eq(#0, #neg(@y)) → #false
#eq(#0, #pos(@y)) → #false
#eq(#0, #s(@y)) → #false
#eq(#neg(@x), #0) → #false
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)
#eq(#neg(@x), #pos(@y)) → #false
#eq(#pos(@x), #0) → #false
#eq(#pos(@x), #neg(@y)) → #false
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)
#eq(#s(@x), #0) → #false
#eq(#s(@x), #s(@y)) → #eq(@x, @y)
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#eq(::(@x_1, @x_2), nil) → #false
#eq(nil, ::(@y_1, @y_2)) → #false
#eq(nil, nil) → #true
#or(#false, #false) → #false
#or(#false, #true) → #true
#or(#true, #false) → #true
#or(#true, #true) → #true

Types:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#less :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #EQ:#GT:#LT
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
insert :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
isortlist :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
isortlist#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
leq#2 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
or :: #false:#true → #false:#true → #false:#true
#or :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_3 :: :::nil:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
gen_:::nil:#0:#neg:#pos:#s4_3 :: Nat → :::nil:#0:#neg:#pos:#s

Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3)) → #false, rt ∈ Ω(0)

Generator Equations:
gen_:::nil:#0:#neg:#pos:#s4_3(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s4_3(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s4_3(x))

The following defined symbols remain to be analysed:
leq, insert, insert#1, isortlist, isortlist#1

They will be analysed ascendingly in the following order:
insert = insert#1
insert < isortlist#1
leq < insert#1
leq = leq#1
isortlist = isortlist#1

(16) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol leq.

(17) Obligation:

Innermost TRS:
Rules:
#equal(@x, @y) → #eq(@x, @y)
#less(@x, @y) → #cklt(#compare(@x, @y))
and(@x, @y) → #and(@x, @y)
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(leq(@x, @y), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insert#2(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys))
isortlist(@l) → isortlist#1(@l)
isortlist#1(::(@x, @xs)) → insert(@x, isortlist(@xs))
isortlist#1(nil) → nil
leq(@l1, @l2) → leq#1(@l1, @l2)
leq#1(::(@x, @xs), @l2) → leq#2(@l2, @x, @xs)
leq#1(nil, @l2) → #true
leq#2(::(@y, @ys), @x, @xs) → or(#less(@x, @y), and(#equal(@x, @y), leq(@xs, @ys)))
leq#2(nil, @x, @xs) → #false
or(@x, @y) → #or(@x, @y)
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)
#eq(#0, #0) → #true
#eq(#0, #neg(@y)) → #false
#eq(#0, #pos(@y)) → #false
#eq(#0, #s(@y)) → #false
#eq(#neg(@x), #0) → #false
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)
#eq(#neg(@x), #pos(@y)) → #false
#eq(#pos(@x), #0) → #false
#eq(#pos(@x), #neg(@y)) → #false
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)
#eq(#s(@x), #0) → #false
#eq(#s(@x), #s(@y)) → #eq(@x, @y)
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#eq(::(@x_1, @x_2), nil) → #false
#eq(nil, ::(@y_1, @y_2)) → #false
#eq(nil, nil) → #true
#or(#false, #false) → #false
#or(#false, #true) → #true
#or(#true, #false) → #true
#or(#true, #true) → #true

Types:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#less :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #EQ:#GT:#LT
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
insert :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
isortlist :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
isortlist#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
leq#2 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
or :: #false:#true → #false:#true → #false:#true
#or :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_3 :: :::nil:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
gen_:::nil:#0:#neg:#pos:#s4_3 :: Nat → :::nil:#0:#neg:#pos:#s

Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3)) → #false, rt ∈ Ω(0)

Generator Equations:
gen_:::nil:#0:#neg:#pos:#s4_3(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s4_3(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s4_3(x))

The following defined symbols remain to be analysed:
insert#1, insert, isortlist, isortlist#1

They will be analysed ascendingly in the following order:
insert = insert#1
insert < isortlist#1
isortlist = isortlist#1

(18) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol insert#1.

(19) Obligation:

Innermost TRS:
Rules:
#equal(@x, @y) → #eq(@x, @y)
#less(@x, @y) → #cklt(#compare(@x, @y))
and(@x, @y) → #and(@x, @y)
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(leq(@x, @y), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insert#2(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys))
isortlist(@l) → isortlist#1(@l)
isortlist#1(::(@x, @xs)) → insert(@x, isortlist(@xs))
isortlist#1(nil) → nil
leq(@l1, @l2) → leq#1(@l1, @l2)
leq#1(::(@x, @xs), @l2) → leq#2(@l2, @x, @xs)
leq#1(nil, @l2) → #true
leq#2(::(@y, @ys), @x, @xs) → or(#less(@x, @y), and(#equal(@x, @y), leq(@xs, @ys)))
leq#2(nil, @x, @xs) → #false
or(@x, @y) → #or(@x, @y)
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)
#eq(#0, #0) → #true
#eq(#0, #neg(@y)) → #false
#eq(#0, #pos(@y)) → #false
#eq(#0, #s(@y)) → #false
#eq(#neg(@x), #0) → #false
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)
#eq(#neg(@x), #pos(@y)) → #false
#eq(#pos(@x), #0) → #false
#eq(#pos(@x), #neg(@y)) → #false
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)
#eq(#s(@x), #0) → #false
#eq(#s(@x), #s(@y)) → #eq(@x, @y)
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#eq(::(@x_1, @x_2), nil) → #false
#eq(nil, ::(@y_1, @y_2)) → #false
#eq(nil, nil) → #true
#or(#false, #false) → #false
#or(#false, #true) → #true
#or(#true, #false) → #true
#or(#true, #true) → #true

Types:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#less :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #EQ:#GT:#LT
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
insert :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
isortlist :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
isortlist#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
leq#2 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
or :: #false:#true → #false:#true → #false:#true
#or :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_3 :: :::nil:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
gen_:::nil:#0:#neg:#pos:#s4_3 :: Nat → :::nil:#0:#neg:#pos:#s

Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3)) → #false, rt ∈ Ω(0)

Generator Equations:
gen_:::nil:#0:#neg:#pos:#s4_3(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s4_3(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s4_3(x))

The following defined symbols remain to be analysed:
insert, isortlist, isortlist#1

They will be analysed ascendingly in the following order:
insert = insert#1
insert < isortlist#1
isortlist = isortlist#1

(20) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol insert.

(21) Obligation:

Innermost TRS:
Rules:
#equal(@x, @y) → #eq(@x, @y)
#less(@x, @y) → #cklt(#compare(@x, @y))
and(@x, @y) → #and(@x, @y)
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(leq(@x, @y), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insert#2(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys))
isortlist(@l) → isortlist#1(@l)
isortlist#1(::(@x, @xs)) → insert(@x, isortlist(@xs))
isortlist#1(nil) → nil
leq(@l1, @l2) → leq#1(@l1, @l2)
leq#1(::(@x, @xs), @l2) → leq#2(@l2, @x, @xs)
leq#1(nil, @l2) → #true
leq#2(::(@y, @ys), @x, @xs) → or(#less(@x, @y), and(#equal(@x, @y), leq(@xs, @ys)))
leq#2(nil, @x, @xs) → #false
or(@x, @y) → #or(@x, @y)
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)
#eq(#0, #0) → #true
#eq(#0, #neg(@y)) → #false
#eq(#0, #pos(@y)) → #false
#eq(#0, #s(@y)) → #false
#eq(#neg(@x), #0) → #false
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)
#eq(#neg(@x), #pos(@y)) → #false
#eq(#pos(@x), #0) → #false
#eq(#pos(@x), #neg(@y)) → #false
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)
#eq(#s(@x), #0) → #false
#eq(#s(@x), #s(@y)) → #eq(@x, @y)
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#eq(::(@x_1, @x_2), nil) → #false
#eq(nil, ::(@y_1, @y_2)) → #false
#eq(nil, nil) → #true
#or(#false, #false) → #false
#or(#false, #true) → #true
#or(#true, #false) → #true
#or(#true, #true) → #true

Types:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#less :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #EQ:#GT:#LT
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
insert :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
isortlist :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
isortlist#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
leq#2 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
or :: #false:#true → #false:#true → #false:#true
#or :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_3 :: :::nil:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
gen_:::nil:#0:#neg:#pos:#s4_3 :: Nat → :::nil:#0:#neg:#pos:#s

Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3)) → #false, rt ∈ Ω(0)

Generator Equations:
gen_:::nil:#0:#neg:#pos:#s4_3(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s4_3(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s4_3(x))

The following defined symbols remain to be analysed:
isortlist#1, isortlist

They will be analysed ascendingly in the following order:
isortlist = isortlist#1

(22) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol isortlist#1.

(23) Obligation:

Innermost TRS:
Rules:
#equal(@x, @y) → #eq(@x, @y)
#less(@x, @y) → #cklt(#compare(@x, @y))
and(@x, @y) → #and(@x, @y)
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(leq(@x, @y), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insert#2(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys))
isortlist(@l) → isortlist#1(@l)
isortlist#1(::(@x, @xs)) → insert(@x, isortlist(@xs))
isortlist#1(nil) → nil
leq(@l1, @l2) → leq#1(@l1, @l2)
leq#1(::(@x, @xs), @l2) → leq#2(@l2, @x, @xs)
leq#1(nil, @l2) → #true
leq#2(::(@y, @ys), @x, @xs) → or(#less(@x, @y), and(#equal(@x, @y), leq(@xs, @ys)))
leq#2(nil, @x, @xs) → #false
or(@x, @y) → #or(@x, @y)
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)
#eq(#0, #0) → #true
#eq(#0, #neg(@y)) → #false
#eq(#0, #pos(@y)) → #false
#eq(#0, #s(@y)) → #false
#eq(#neg(@x), #0) → #false
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)
#eq(#neg(@x), #pos(@y)) → #false
#eq(#pos(@x), #0) → #false
#eq(#pos(@x), #neg(@y)) → #false
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)
#eq(#s(@x), #0) → #false
#eq(#s(@x), #s(@y)) → #eq(@x, @y)
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#eq(::(@x_1, @x_2), nil) → #false
#eq(nil, ::(@y_1, @y_2)) → #false
#eq(nil, nil) → #true
#or(#false, #false) → #false
#or(#false, #true) → #true
#or(#true, #false) → #true
#or(#true, #true) → #true

Types:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#less :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #EQ:#GT:#LT
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
insert :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
isortlist :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
isortlist#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
leq#2 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
or :: #false:#true → #false:#true → #false:#true
#or :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_3 :: :::nil:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
gen_:::nil:#0:#neg:#pos:#s4_3 :: Nat → :::nil:#0:#neg:#pos:#s

Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3)) → #false, rt ∈ Ω(0)

Generator Equations:
gen_:::nil:#0:#neg:#pos:#s4_3(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s4_3(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s4_3(x))

The following defined symbols remain to be analysed:
isortlist

They will be analysed ascendingly in the following order:
isortlist = isortlist#1

(24) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol isortlist.

(25) Obligation:

Innermost TRS:
Rules:
#equal(@x, @y) → #eq(@x, @y)
#less(@x, @y) → #cklt(#compare(@x, @y))
and(@x, @y) → #and(@x, @y)
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(leq(@x, @y), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insert#2(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys))
isortlist(@l) → isortlist#1(@l)
isortlist#1(::(@x, @xs)) → insert(@x, isortlist(@xs))
isortlist#1(nil) → nil
leq(@l1, @l2) → leq#1(@l1, @l2)
leq#1(::(@x, @xs), @l2) → leq#2(@l2, @x, @xs)
leq#1(nil, @l2) → #true
leq#2(::(@y, @ys), @x, @xs) → or(#less(@x, @y), and(#equal(@x, @y), leq(@xs, @ys)))
leq#2(nil, @x, @xs) → #false
or(@x, @y) → #or(@x, @y)
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)
#eq(#0, #0) → #true
#eq(#0, #neg(@y)) → #false
#eq(#0, #pos(@y)) → #false
#eq(#0, #s(@y)) → #false
#eq(#neg(@x), #0) → #false
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)
#eq(#neg(@x), #pos(@y)) → #false
#eq(#pos(@x), #0) → #false
#eq(#pos(@x), #neg(@y)) → #false
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)
#eq(#s(@x), #0) → #false
#eq(#s(@x), #s(@y)) → #eq(@x, @y)
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#eq(::(@x_1, @x_2), nil) → #false
#eq(nil, ::(@y_1, @y_2)) → #false
#eq(nil, nil) → #true
#or(#false, #false) → #false
#or(#false, #true) → #true
#or(#true, #false) → #true
#or(#true, #true) → #true

Types:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#less :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #EQ:#GT:#LT
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
insert :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
isortlist :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
isortlist#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
leq#2 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
or :: #false:#true → #false:#true → #false:#true
#or :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_3 :: :::nil:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
gen_:::nil:#0:#neg:#pos:#s4_3 :: Nat → :::nil:#0:#neg:#pos:#s

Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3)) → #false, rt ∈ Ω(0)

Generator Equations:
gen_:::nil:#0:#neg:#pos:#s4_3(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s4_3(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s4_3(x))

No more defined symbols left to analyse.

(26) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(1) was proven with the following lemma:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3)) → #false, rt ∈ Ω(0)

(27) BOUNDS(1, INF)

(28) Obligation:

Innermost TRS:
Rules:
#equal(@x, @y) → #eq(@x, @y)
#less(@x, @y) → #cklt(#compare(@x, @y))
and(@x, @y) → #and(@x, @y)
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(leq(@x, @y), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insert#2(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys))
isortlist(@l) → isortlist#1(@l)
isortlist#1(::(@x, @xs)) → insert(@x, isortlist(@xs))
isortlist#1(nil) → nil
leq(@l1, @l2) → leq#1(@l1, @l2)
leq#1(::(@x, @xs), @l2) → leq#2(@l2, @x, @xs)
leq#1(nil, @l2) → #true
leq#2(::(@y, @ys), @x, @xs) → or(#less(@x, @y), and(#equal(@x, @y), leq(@xs, @ys)))
leq#2(nil, @x, @xs) → #false
or(@x, @y) → #or(@x, @y)
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)
#eq(#0, #0) → #true
#eq(#0, #neg(@y)) → #false
#eq(#0, #pos(@y)) → #false
#eq(#0, #s(@y)) → #false
#eq(#neg(@x), #0) → #false
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)
#eq(#neg(@x), #pos(@y)) → #false
#eq(#pos(@x), #0) → #false
#eq(#pos(@x), #neg(@y)) → #false
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)
#eq(#s(@x), #0) → #false
#eq(#s(@x), #s(@y)) → #eq(@x, @y)
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#eq(::(@x_1, @x_2), nil) → #false
#eq(nil, ::(@y_1, @y_2)) → #false
#eq(nil, nil) → #true
#or(#false, #false) → #false
#or(#false, #true) → #true
#or(#true, #false) → #true
#or(#true, #true) → #true

Types:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#less :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #EQ:#GT:#LT
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
insert :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
isortlist :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
isortlist#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
leq#2 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
or :: #false:#true → #false:#true → #false:#true
#or :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_3 :: :::nil:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
gen_:::nil:#0:#neg:#pos:#s4_3 :: Nat → :::nil:#0:#neg:#pos:#s

Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3)) → #false, rt ∈ Ω(0)

Generator Equations:
gen_:::nil:#0:#neg:#pos:#s4_3(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s4_3(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s4_3(x))

No more defined symbols left to analyse.

(29) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(1) was proven with the following lemma:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3)) → #false, rt ∈ Ω(0)

(30) BOUNDS(1, INF)